ds:x:Id fp Type, da:k:Knd fp Type, A, B:ecl-trans-tuple{i:l}(ds;da), f:(()()),
g:().
ecl-trans-normal(A)
 ecl-trans-normal(B)
 (m:. f((n.false),n.false,m))
 ecl-trans-normal(combine-ecl-tuples(A;B;f;g)) 

latex

Definitions	t  T, x:A. B(x), b, P  Q, False, A, AB, , P  Q, P & Q, P  Q, Prop, True, T, , x. t(x), , no_repeats(T;l), sorted(L), finite-type(T), Dec(P), let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), ecl-trans-normal(x), combine-ecl-tuples(A;B;f;g), ecl-trans-tuple{i:l}(ds;da), Id, a:A fp B(a), Knd, false
Lemmas	bfalse wf, ecl-trans-normal wf, ecl-trans-tuple wf, Knd wf, fpf wf, Id wf, decidable equal product, no repeats-merge, sorted-merge, nat plus wf, finite-type-product, not wf, assert wf, squash wf, true wf, bool wf, nat wf, eqff to assert, assert of bnot